# Алгебра Гейтинга и Bool

## Алгебра Гейтинга

Алгебра Гейтинга представляют собой ограниченные решетки, 
которые также снабжены дополнительной бинарной операцией `imp` (для импликации, также записываемой как `→`).

Импликация подчиняется следующим законам:

- `a → a = 1`
- `a ∧ (a → b) = a ∧ b`
- `b ∧ (a → b) = b`
- `a → (b ∧ c) = (a → b) ∧ (a → c)`

В алгебрах Гейтинга `and` эквивалентно `meet` и `or` эквивалентно `join`; доступны оба метода.

Алгебра Гейтинга также определяет операцию дополнения (`complement`) (иногда записываемую как `¬a`). 
Дополнение к `a` эквивалентно (`a → 0`), и выполняются следующие законы:

- `а ∧ ¬а = 0`

Однако в алгебрах Гейтинга эта операция является лишь псевдодополнением, 
поскольку алгебры Гейтинга не обязательно обеспечивают закон исключенного третьего. 
Это означает, что нет никакой гарантии, что `(a ∨ ¬a) = 1`.

Алгебры Гейтинга моделируют интуиционистскую логику. 
Для модели классической логики см. ниже класс типов булевой алгебры, реализованный как `Bool`.

`Heyting[A]` - типы, образующие алгебру Гейтинга

- `complement` (унарное `~`): логическое отрицание
- `and` (`&`, `meet`): конъюнкция ("И")
- `or` (`|`, `join`): дизъюнкция ("ИЛИ")
- `xor` (`^`): исключающее дизъюнкция: `or(and(a, complement(b)), and(complement(a), b))`
- `imp`: следствие ("НЕ a или b"), эквивалентно `~a | b`
- `nand`: "не И", эквивалентно `~(a & b)`: `complement(and(a, b))`
- `nor`: "не ИЛИ", эквивалентно `~(a | b)`: `complement(or(a, b))`
- `nxor`: "не xor", эквивалентно `~(a ^ b)`: `complement(xor(a, b))`

## Bool

`Bool` поддерживает булеву алгебру — абстракцию знакомых побитовых логических операторов.

Булевы алгебры являются алгебрами Гейтинга с дополнительным ограничением, 
заключающимся в истинности закона исключенного третьего (что эквивалентно истинному двойному отрицанию).
Это означает, что помимо законов, которым подчиняются алгебры Гейтинга, булевы алгебры также подчиняются следующим:

- `(а ∨ ¬а) = 1`
- `¬¬а = а`

Булевы алгебры обобщают классическую логику: единица эквивалентна "истине", а ноль эквивалентен "ложности". 
Булевы алгебры предоставляют дополнительные часто используемые логические операторы, такие как `xor`, `nand`, `nor` и `nxor`.
У каждой булевой алгебры есть двойственная алгебра, которая включает в себя изменение местами истинное/ложное, а также и/или.

- `complement` (унарное `~`): логическое отрицание
- `and` (`&`, `meet`): конъюнкция ("И")
- `or` (`|`, `join`): дизъюнкция ("ИЛИ")
- `xor` (`^`): исключающее дизъюнкция: `or(and(a, complement(b)), and(complement(a), b))`
- `imp`: следствие ("НЕ a или b"), эквивалентно `~a | b`
- `nand`: "не И", эквивалентно `~(a & b)`: `complement(and(a, b))`
- `nor`: "не ИЛИ", эквивалентно `~(a | b)`: `complement(or(a, b))`
- `nxor`: "не xor", эквивалентно `~(a ^ b)`: `complement(xor(a, b))`

Экземпляры `Bool` существуют не только для `Boolean`, 
но и для `Byte`, `Short`, `Int`, `Long`, `UByte`, `UShort`, `UInt` и `ULong`.

---

**Ссылки:**

- [Spire home page](https://typelevel.org/spire)
- [Learning Spire - Boolean Algebras are pretty cool](https://www.chrisstucchio.com/blog/2013/learning_spire_boolean_algebra.html)
